Iof proof for Lemma bool cases sqequal:
b:
. (b ~ tt) 
(b ~ ff)
by ((D 0)
THENW ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
T) inil_term)))
T1:
T1: 1. b :
T1: (b ~ tt) (b ~ ff)
T.| 12,41 |
b:. (b ~ tt) (b ~ ff)
by ((D 0)
THENW ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
T) inil_term)))
T1:
T1: 1. b :
T1: (b ~ tt) (b ~ ff)
T.
| Definitions |  Tx:A. B(x) |
| Lemmas |